$\vdash$  $\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). \{!$x$:$T$ $\mid$ $P$($x$)\} $\in$ Type